\begin{tabbing}
$\forall$\=$D$:Dsys, $i$:Id, $s_{1}$, $s_{2}$:M($i$).state, $k_{1}$, $k_{2}$:Knd, $v_{1}$:d{-}decl($D$;$i$)($k_{1}$), $v_{2}$:d{-}decl($D$;$i$)($k_{2}$),\+
\\[0ex]$m_{1}$:\{$m$:M($i$).Msg$\mid$ source(mlnk($m$)) $=$ $i$ \} List.
\-\\[0ex]Feasible($D$)
\\[0ex]$\Rightarrow$ $\langle$$s_{1}$$,\,$doact($k_{1}$;$v_{1}$)$,\,$$m_{1}$$\rangle$ $=$ next{-}world{-}state($D$;$i$;$s_{2}$;$k_{2}$;$v_{2}$) $\in$ d{-}world{-}state($D$;$i$)
\\[0ex]$\Rightarrow$ \{\=$s_{1}$ $=$ ($\lambda$$x$.M($i$).ef($k_{2}$,$x$,$s_{2}$,$v_{2}$)?$s_{2}$($x$))\+
\\[0ex]\& $k_{1}$ $=$ $k_{2}$
\\[0ex]\& $v_{1}$ $=$ $v_{2}$ $\in$ d{-}decl($D$;$i$)($k_{2}$)
\\[0ex]\& $m_{1}$ $=$ filter($\lambda$$m$.source(mlnk($m$)) = $i$;M($i$).sends($k_{2}$,$s_{2}$,$v_{2}$))\}
\-
\end{tabbing}